Problem:
 and(tt(),X) -> X
 plus(N,0()) -> N
 plus(N,s(M)) -> s(plus(N,M))

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {5,4}
   transitions:
    s1(6) -> 6,5
    plus1(3,1) -> 6*
    plus1(3,3) -> 6*
    plus1(1,2) -> 6*
    plus1(2,1) -> 6*
    plus1(2,3) -> 6*
    plus1(3,2) -> 6*
    plus1(1,1) -> 6*
    plus1(1,3) -> 6*
    plus1(2,2) -> 6*
    and0(3,1) -> 4*
    and0(3,3) -> 4*
    and0(1,2) -> 4*
    and0(2,1) -> 4*
    and0(2,3) -> 4*
    and0(3,2) -> 4*
    and0(1,1) -> 4*
    and0(1,3) -> 4*
    and0(2,2) -> 4*
    tt0() -> 1*
    plus0(3,1) -> 5*
    plus0(3,3) -> 5*
    plus0(1,2) -> 5*
    plus0(2,1) -> 5*
    plus0(2,3) -> 5*
    plus0(3,2) -> 5*
    plus0(1,1) -> 5*
    plus0(1,3) -> 5*
    plus0(2,2) -> 5*
    00() -> 2*
    s0(2) -> 3*
    s0(1) -> 3*
    s0(3) -> 3*
    1 -> 6,5,4
    2 -> 6,5,4
    3 -> 6,5,4
  problem:
   
  Qed